D:Dsys. Feasible(D)  i:IdM(i).state 

latex

Definitions	x:A. B(x), f(x)?z, 1of(t), Top, P  Q, M.state, Feasible(D), t  T, xdom(f). v=f(x)   P(x;v), Feasible(M), P & Q, Unit, P  Q, Prop, , MsgA, x. t(x), , State(ds)
Lemmas	top wf, fpf wf, fpf-trivial-subtype-top, msga wf, d-m wf, assert wf, not wf, bnot wf, bool wf, id-deq wf, fpf-dom wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, dsys wf, d-feasible wf, Id wf